[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification ubi-quality-base
enrich
   ubi-asm
with
   

   
   
   functions  Δ . : wlarray → nat;
              ecs : wlarray → nat-bag;
              ecs : wlarray × nat → nat-bag;
              sum-of-differences : nat × nat-bag → nat;
   
   
   
   
   

   

   axioms threshold-ge-erase-retries :  ⊦ ¬ WL_THRESHOLD ≤ UBI_ERASE_RETRIES;
          used for: s, ls;
          ecs :  ⊦ ecs(wlar) = ecs(wlar, # wlar);
          ecs-n-base :  ⊦ ecs(wlar, 0) = ∅;
          used for: s, ls;
          ecs-n-rec :  ⊦ n < # wlar → ecs(wlar, n + 1) = ecs(wlar, n) ++ wlar[n].ec;
          used for: ls;
          sum-of-differences-base :  ⊦ sum-of-differences(n, ∅) = 0;
          used for: s, ls;
          sum-of-differences-rec :  ⊦ sum-of-differences(n, bag ++ m) = (n - m) + sum-of-differences(n, bag);
          used for: s, ls;
          delta :  ⊦ Δ wlar = sum-of-differences(ecs(wlar).max, ecs(wlar));
          used for: ls;

   

   
end enrich